| Definitions | null(as),  A, False, P  Q, (e < e'), strong-subtype(A;B), a:A fp B(a),  , Type, E, e c e', f(a), f**(e), prior-f-fixedpoints(e), Top, {x:A| B(x)} ,  x:A. B(x), a < b, left + right,  b, x:A  B(x), (x  l), s = t, ES, AbsInterface(A), t T, P   Q,  x:A. B(x), x:A B(x), E(X), e  X, let x,y = A in B(x;y), P & Q, constant_function(f;A;B),  , r s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , type List, Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),   x,y. t(x;y), x. t(x), Knd, EState(T), EOrderAxioms(E; pred?; info), Id, IdLnk, Unit, EqDecider(T), True, P  Q, A c B, |g|, l[i], Void, ||as||, A B, #$n, Outcome,  , A List , S  T, [], f(x)?z, x.A(x), kind(e), loc(e), [car / cdr], <a, b> |